package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.IndividualNameManager;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.syntax.concept.BooleanConcept;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.concept.RoleQuantification;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.RoleInclusion;


/**
 * 
 * @author İnanç Seylan
 *
 */
public class NegatedRoleInclusionRule extends CompletionRule {
	private ABox aBox;

	private boolean applied;

	public NegatedRoleInclusionRule() {
		super();
	}

	public NegatedRoleInclusionRule(WorldConstraintSystem wcs, World world) {
		super(wcs, world);
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		for (RoleInclusion ri : getWorld().getRBox().getNegatedInclusions()) {
			ConceptName c = new ConceptName(" C");
			Concept negRIEqualConcept = new BooleanConcept(
					BooleanConcept.Constructor.INTERSECTION,
					new RoleQuantification(RoleQuantification.Constructor.SOME,
							ri.getLhs(), c), new RoleQuantification(
							RoleQuantification.Constructor.ALL, ri.getRhs(), c
									.copy().toggleNegated()));
			boolean alreadyExists = false;
			for (Iterator<Individual> i = aBox.individualIterator(); i
					.hasNext();) {
				Individual indv = i.next();
				if (aBox.contains(new ConceptAssertion(negRIEqualConcept, indv
						.getName()))) {
					alreadyExists = true;
					break;
				}
			}
			if (!alreadyExists) {
				String newIndv = IndividualNameManager.getInstance()
						.generateIndividualName();
				ConceptAssertion ca = new ConceptAssertion(negRIEqualConcept,
						newIndv);
				getWcs().getData().getLogger().info(
						"WCS " + getWcs().getId()
								+ " Negated role inclusion rule: Generating "
								+ newIndv + " adding " + ca);
				aBox.add(ca);
				applied = true;
			}
		}
	}

	public boolean isApplied() {
		return applied;
	}
}
